(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun aa () Real)
(assert (not (exists ((g Real)) (=> (and (< (- (* (- (- h (- 24)) 1) (* (- (+ h (/ 8 k) (- k))) (* (+ 149 k) e)))) (- b d)) (> e (+ 8 a) (* b d) 86) (> (/ 1 c i) (/ a j j))) (< e 0)))))
(assert (= (- k f) (- aa)))
(check-sat)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun aa () Real)
(assert (not (exists ((g Real)) (=> (and (< (- (* (- (- h (- 24)) 1) (* (- (+ h (/ 8 k) (- k))) (* (+ 149 k) e)))) (- b d)) (> e (+ 8 a) (* b d) 86) (> (/ 1 c i) (/ a j j))) (< e 0)))))
(assert (= (- k f) (- aa)))
(check-sat)
